COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	SECTION 6. Question Answering.
C00005 ENDMK
C⊗;
SECTION 6. Question Answering.
.SKIP 3
.BEGIN DOUBLE SPACE
A subset of the Luckham-Nilsson answer-extraction algorithm has been implemented.
It is not  available as part of the basic prover, but must be loaded by the user.
The prover should be run in  slightly more core to accommodate the answer routines.

Here is an example:

.BEGIN VERBATIM
Recall example 2. in the introduction:

(1) ∀(x,y)P(x,y)∧P(y,z)⊃G(x,z)
(2) ∀y∃xP(x,y)
Question:(3) ∃(x,y)G(x,y) .
.END

From the semantics of the problem we know that the "answer" to (3) is
"yes" and in fact we can display specific solutions to the problem:  The
parent of the parent  is the grandparent.
What does the answer extractor do with this problem?


.BEGIN VERBATIM

R PROVER		;get the prover
(DSKIN (P,JRA) ANSWER)	;load in answer extractor 
(PROVE DSK: EX2)	
    ...
[output as before]
    ...
*(ANSWER)		;this calls the extractor
*G(G21(G21(x)),x)	;the answer
*
.END
We must now interpret the Skolem function G21.  G21 was introduced in the
translation of (2), that is, G21(y) is an object such that P(G21(y),y).
Thus G21 is a function to select the parent of an individual.  In this
light our answer, G(G21(G21(x)),x), is the expected result.

The current implementation of the answer extractor does not  recognize
applications of the equality rule and will fail to get answers in this case.
It is trivial to extend the algorithm and its implementation will occur
shortly.

.END